ABS: R-pre-init(i;ds;init;a;T;P)

STM: R-pre-init wf

STM: R-pre-init-feasible

ABS: R-pre-init1(i;x;A;x0;a;T;P)

STM: R-pre-init1 wf

STM: R-pre-init1-feasible

ABS: MsgFrom(i)

STM: w-Msg-from wf

STM: better-w-m-wf

ABS: (x initially i)

STM: w-initially wf

ABS: first(e)

STM: w-first-aux

STM: w-first wf

STM: assert-w-first

STM: w-loc-time

STM: better-w-sends-wf

STM: w-causl-time-iff

STM: decl-rename-cap

ABS: action-rename(rainv;rtinv;a)

STM: action-rename wf

ABS: world-rename(rx;ra;rt;rainv;rtinv;w)

STM: world-rename wf

STM: es-kindtype-w-valtype

ABS: d(e;e')

STM: w-d wf

STM: w-d-properties

ABS: Kind(da)

STM: ma-kind wf

ABS: MsgA(ds;da)

STM: msga-body wf

STM: msga-factor

ABS: Shape(M)

STM: ma-shape wf

ABS: ma-body(M)

STM: ma-body wf

STM: msga-subtype

ABS: M.X

STM: ma-X wf

ABS: M.A

STM: ma-A wf

ABS: x declared in M

STM: ma-declx wf

STM: decidable ma-declx

STM: not-ma-declx-implies

ABS: k declared in M

STM: ma-declk wf

STM: not-ma-declk-implies

STM: decidable ma-declk

STM: decidable ma-declm

ABS: da-outlink-f(da;k)

STM: da-outlink-f wf

ABS: da-outlinks(da;i)

STM: da-outlinks wf

STM: da-outlinks-empty

STM: da-outlinks-single

STM: da-outlinks-join

ABS: ma-outlinks(M;i)

STM: ma-outlinks wf

STM: din-not-declared

ABS: tag tg always has type T in M

STM: ma-tag-type wf

ABS: M.kind

STM: ma-k wf

ABS: ma-has-effect(M;k)

STM: ma-has-effect wf

STM: ma-no-effect

STM: decidable ma-has-effect

ABS: ma-has-sends(M;k)

STM: ma-has-sends wf

STM: decidable ma-has-sends

ABS: sends-on-pair(s;l;tg)

STM: sends-on-pair wf

STM: assert-sends-on-pair

STM: ma-no-sends

STM: ma-dout2-subtype

STM: ma-rframe-pre wf

STM: ma-rframe-ef wf

STM: ma-rframe-send wf

STM: ma-sub transitivity

ABS: ma-is-empty(M)

STM: ma-is-empty wf

STM: assert-ma-is-empty

STM: ma-empty-is-empty

STM: ma-empty-sub

STM: ma-is-empty-sub

STM: ma-empty-tag-type

STM: ma-compatible-decls wf

STM: ma-join-empty

STM: ma-empty-join

STM: ma-comp-decls-join

STM: ma-join-assoc

STM: ma-compatible weakening

STM: ma-join-sub

ABS: with declarations ds:dsda:da

STM: ma-single-decls wf

ABS: ma-single-effect0(x;A;k;T;f)

STM: ma-single-effect0 wf

ABS: ma-single-effect1(x;A;y;B;k;T;f)

STM: ma-single-effect1 wf

ABS: ma-single-sends0(B;T;a;l;tg;f)

STM: ma-single-sends0 wf

ABS: a(v) sends [tg,   f(x, v)] on link l  

ABS: ma-single-pre1(x;A;a;T;y,v.P(y;v))

STM: ma-single-pre1 wf

ABS: precondition a: True

STM: ma-single-pre-true wf

ABS: with ds: ds init: initaction a:T precondition a(v) is P

STM: ma-single-pre-init wf

ABS: ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v))

STM: ma-single-pre-init1 wf

STM: ma-state-atom-free

STM: ma-da-atom-free

STM: ma-dout-atom-free

ABS: (L)

STM: ma-join-list-property

STM: ma-join-list wf

STM: ma-sub-join-list

STM: ma-join-list-feasible

STM: ma-join-list-compat

STM: ma-join-list-compat2

STM: ma-join-declm

STM: ma-join-list-declm

STM: ma-join-list-declm2

STM: ma-join-list-din

STM: ma-join-list-dout

ABS: MsgAForm

STM: msg-form wf

STM: msga-sub-msg-form

STM: ma-outlinks-wf2

STM: msg-form-join

STM: msg-form-join-list

STM: ma-is-empty wf join

STM: ma-join-list-is-empty

STM: assert-ma-join-list-is-empty

STM: ma-outlinks-join

STM: ma-outlinks-join-list

STM: sub-join-list-din

STM: ma-join-list-tag-type

ABS: ma-rename(rx;ra;rt;M)

STM: ma-rename wf

STM: msga-at-sub-left

STM: msga-at-sub-right

STM: ma-single-init-feasible

STM: ma-single-frame-feasible

STM: ma-single-sframe-feasible

STM: ma-single-pre-init1-feasible

STM: ma-single-pre-init-feasible

STM: ma-single-effect-feasible

STM: ma-single-effect0-feasible

STM: ma-single-pre-true-feasible

STM: ma-single-pre-feasible

STM: ma-single-pre1-feasible

STM: ma-single-sends-feasible

ABS: Chooser(dec)

STM: ma-chooser wf

ABS: Trans(M)

STM: ma-trans wf

ABS: Sends(M)

STM: ma-sends wf

STM: ma-atom-free

STM: atom-free-ma-state

STM: atom-free-ma-decider

STM: atom-free-ma-shape

STM: atom-free-ma-msg-from

STM: ma-init-val-inherence

STM: ma-ef-val-inherence

STM: ma-send-val-inherence

ABS: Inlnk(i)

STM: d-I wf

ABS: Outlnk(i)

STM: d-O wf

ABS: d-empty()

STM: d-empty wf

STM: d-sub-null

STM: d-sub transitivity

ABS: @i: with declarations ds:ds da:da

STM: d-single-decls wf

ABS: @i (with ds: ds init: init action a:T precondition a(v) is P s v)

STM: d-single-pre-init wf

STM: d-feasible-types

STM: d-feasible-types2

STM: d-decl-atom-free

STM: equal-d-world-states

ABS: local-atom(A;dec;a)

STM: local-atom wf

ABS: onlnk(l;mss)

STM: d-onlnk wf

ABS: d-rename(rx;ra;rt;D)

STM: d-rename wf

ABS: interface-check(D;l;tg;T)

STM: interface-check wf

STM: interface-check-tag-type

STM: finite-support-feasible

STM: finite-support-interface-feasible

STM: atom-free-d-msg-from

STM: ma-dout-sub

STM: realizes-monotone-wrt-sub

ABS: Decl

STM: s-decl wf

ABS: 

STM: s-decl-null wf

ABS: d(a)

STM: s-declared wf

STM: m-at wf

ABS: InDecl(i)

STM: in-decl wf

ABS: OutDecl(i)

STM: out-decl wf

ABS: d(p)

ABS: d(p)

STM: s-out-declared wf

STM: s-in-declared wf

ABS: Valtype(k;da;din)

STM: s-valtype wf

ABS: s-state(ds)

STM: s-state wf

STM: m-sys-compatible-symmetry

STM: m-at-compatible

STM: m-at-distinct-compatible

STM: m-at-self-compatible

STM: m-sys-compatible-join

STM: interface-compatible-at-same

STM: m-sys-sub-join-left

STM: m-sys-sub-join-right

STM: dsys-join-sub

ABS: (L)

STM: m-sys-join-list-property

STM: dsys-join-list-property

STM: m-sys-join-list wf

STM: m-sys-join-list wf2

STM: m-sys-sub-join-list

STM: m-sys-sub-join-map

STM: m-sys-join-list-property2

STM: join-list-compatible

STM: join-list-compatible2

STM: interface-compatible-join-list

STM: interface-compatible-join-list2

STM: feasible-join-list

STM: ma-single-pre1 wf2

STM: ma-single-effect0 wf2

ABS: s-dsys(M)

STM: s-dsys wf

ABS: DsysNull

STM: dsys-null wf

STM: s-at-sub-s-dsys

STM: s-at-sub-s-at

STM: s-dsys-sub-s-dsys

STM: dsys-single-sub-dsys

ABS: Rcv(l;tg)

STM: Rcv wf

STM: s-pre-rule

STM: s-pre-rule0

STM: s-pre-rule1

STM: s-effect-rule

STM: s-effect-rule0

STM: effect-rule1

STM: s-sends-rule

STM: ma-single-sends1 wf

STM: s-sends-rule1

STM: s-unconditional-send1-rule

STM: conditional-send1-rule

STM: sends-rule0

STM: unconditional-send-rule0

STM: s-init-rule

STM: s-frame-rule

STM: frame-rule0

STM: frame-rule1

STM: frame-rule2

STM: frame-rule3

STM: s-sframe-rule

STM: better-sframe-rule

STM: ma-component-types

ABS: effect-type(ds;ds';da)

STM: effect-type wf

STM: effect-type-subtype

STM: proper-at-join

STM: m-sys-feasible

STM: msys-at-compatible-right

STM: msys-at-compatible-left

STM: msys-at-at

STM: ma-single-pre-init-ma-single-pre-compatible

STM: ma-single-pre-ma-single-pre-init-compatible

STM: ma-single-pre-init-ma-single-sends-compatible

STM: ma-single-sends-ma-single-pre-init-compatible

STM: ma-single-pre-init-ma-single-effect-compatible

STM: ma-single-effect-ma-single-pre-init-compatible

STM: ma-single-pre-init-ma-single-sframe-compatible

STM: ma-single-sframe-ma-single-pre-init-compatible

STM: ma-single-pre-init-ma-single-frame-compatible

STM: ma-single-frame-ma-single-pre-init-compatible

STM: ma-single-pre-init-ma-single-init-compatible

STM: ma-single-init-ma-single-pre-init-compatible

STM: ma-single-pre-ma-single-sends-compatible

STM: ma-single-sends-ma-single-pre-compatible

STM: ma-single-pre-ma-single-effect-compatible

STM: ma-single-effect-ma-single-pre-compatible

STM: ma-single-pre-ma-single-sframe-compatible

STM: ma-single-sframe-ma-single-pre-compatible

STM: ma-single-pre-ma-single-frame-compatible

STM: ma-single-frame-ma-single-pre-compatible

STM: ma-single-pre-ma-single-init-compatible

STM: ma-single-init-ma-single-pre-compatible

STM: ma-single-sends-ma-single-effect-compatible

STM: ma-single-effect-ma-single-sends-compatible

STM: ma-single-sends-ma-single-sframe-compatible

STM: ma-single-sframe-ma-single-sends-compatible

STM: ma-single-sends-ma-single-frame-compatible

STM: ma-single-frame-ma-single-sends-compatible

STM: ma-single-sends-ma-single-init-compatible

STM: ma-single-init-ma-single-sends-compatible

STM: ma-single-effect-ma-single-sframe-compatible

STM: ma-single-sframe-ma-single-effect-compatible

STM: ma-single-effect-ma-single-frame-compatible

STM: ma-single-frame-ma-single-effect-compatible

STM: ma-single-effect-ma-single-init-compatible

STM: ma-single-init-ma-single-effect-compatible

STM: ma-single-sframe-ma-single-frame-compatible

STM: ma-single-frame-ma-single-sframe-compatible

STM: ma-single-sframe-ma-single-init-compatible

STM: ma-single-init-ma-single-sframe-compatible

STM: ma-single-frame-ma-single-init-compatible

STM: ma-single-init-ma-single-frame-compatible

STM: ma-single-pre-init-ma-single-pre-init-compatible

STM: ma-single-pre-ma-single-pre-compatible

STM: ma-single-sends-ma-single-sends-compatible

STM: ma-single-effect-ma-single-effect-compatible

STM: ma-single-sframe-ma-single-sframe-compatible

STM: ma-single-frame-ma-single-frame-compatible

STM: ma-single-init-ma-single-init-compatible

STM: m-sys-at-sub-lemma1

STM: d-sub-lemma1

STM: ma-sub-join-mapl

STM: R-Dsys-Rall2

STM: R-Dsys-Rall

STM: R-Dsys-Rall-init

STM: R-Dsys-sub-Rall

STM: R-sub-feasible-Dsys

STM: R-state-property

STM: R-da-property

STM: R-ds-property

STM: R-Feasible-interface

ABS: R-init(R;i)

STM: R-init wf

STM: R-Feasible-action